| Model: | embedded v.1 (CTMC) |
| Parameter(s) | MAX_COUNT = 8, T = 12 |
| Property: | actuators (prob-reach) |
java -Xms10240m -Xmx10240m -jar ./root/epmc-standard.jar check --model-input-files embedded.prism --model-input-type prism --property-input-files embedded.props --property-input-names actuators --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const MAX_COUNT=8,T=12
| Walltime: | 6.608355283737183s |
| Return code: | 0 |
| Note(s): | The tool result '103508293133187/1000000000000000' is tagged as incorrect. The reference result is '2486339329126654286603009697501669410565922080647235572297420531003436740865701642894224651957236979415804844019970070797212838741320749871087696043790430488516768144231337033817746564261751745074561347394006816495027017797689319547300488225074500148562849173672852142305219348461967484204844049064729196699735928014471258755257981315981437194941990940151801223037104684834501918219518509576147895594521550143080313306069328271572867233516691965651482621705351476665971739605138196440899155147689763504549588268208121401875264463514032072760483012146809591389917819090345027584564812047944749664670576370371539376963526238191240909958985452275278006429583432435031807238331342878089585624527146895090748546393263058273883548791148930403418281798548198424839109773636808627978181634014955673865189747661646872651996258392552936446048778850218123619968642035042613279480618036150872134108049644406926052409061681799637826350380022669199996003596956454782552145333056157894145489486150540020412367389756815095367155100979032989577219964876141639524244527608740339422128257119204903748534580255367130745069830155822896692205418889181867570399342666796568670310583910515081237965368477709014032538181219194690388788147910806457016503932544044361342482618424045300689342156932654513810653232/23611139712102051230917389163705830960031855919193061353466918264830083378326191986369644719731733927229539492600419384037259194731474764121283541927110582338954972260482489069672524784993784262550354865456872177586787640220120819688039079785300002792915291730955593483931646644219725546280035297145057925920216590907280123192615618204899469159482885775117640880607396241557854775904114044868093404127365731780383766098536743365431606149805147123738769862714193052746662633506746823832901275751745965930188386773348462353851130634494111719846304545619011283033383773694078253680336971342463788449790335853827682934039541430969389834393278233712786556823508225268957600063594542555015850051657407051988438160129534133247921531327619001040045086238243881240503946765414870850573700427770606192511529412103367398696559809991483002140786128316014280845971470100880405232693440182197432483126227685144563355464988202359315240457890538240804613319209327258473954661426136227180487183808347011148390279684571713981594509718194717843432940624635810976882203361528885015337153218704100617865345448218447207127579308191723103792137390005496384380796220104269395092237919302086773300230575431863081466614429004067089423894856968938002028941688162575178715549796054402371237245066557533118053584375' (approx. 0.1053036557931282) which means a relative error of '0.01704938585862802' which is larger than the goal precision '0.001'. |
| Relative Error: | 0.01704938585862802 |
assertions-disabled start-parsing done-parsing model-checking analysing-property actuators start-building-explorer start-building-initial-states-explorer done-building-initial-states-explorer done-building-explorer build-model-start build-model-done 8548 0 iterating iterating-progress-unbounded 20908 6.645653838549512E-5 1 iterating-progress-unbounded 43441 1.6961577883547007E-5 2 iterating-progress-unbounded 65957 4.981695852250649E-6 3 iterating-progress-unbounded 88480 1.4342460008567787E-6 4 iterating-done 94859 4 model-checking-done 5 command-check-result-is 0.103508293133187 actuators